/* mockturtle: C++ logic network library
 * Copyright (C) 2018-2021  EPFL
 *
 * Permission is hereby granted, free of charge, to any person
 * obtaining a copy of this software and associated documentation
 * files (the "Software"), to deal in the Software without
 * restriction, including without limitation the rights to use,
 * copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the
 * Software is furnished to do so, subject to the following
 * conditions:
 *
 * The above copyright notice and this permission notice shall be
 * included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
 * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
 * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
 * OTHER DEALINGS IN THE SOFTWARE.
 */

/*!
  \file xag_npn.hpp
  \brief Replace with size-optimum XAGs and AIGs from NPN (from ABC rewrite)

  \author Heinz Riener
  \author Mathias Soeken
  \author Siang-Yun (Sonia) Lee
*/

#pragma once

#include <algorithm>
#include <cstdint>
#include <vector>

#include <fmt/format.h>
#include <kitty/constructors.hpp>
#include <kitty/dynamic_truth_table.hpp>
#include <kitty/npn.hpp>
#include <kitty/print.hpp>
#include <kitty/static_truth_table.hpp>

#include "../../algorithms/simulation.hpp"
#include "../../networks/xag.hpp"
#include "../../utils/index_list.hpp"
#include "../../utils/node_map.hpp"
#include "../../utils/stopwatch.hpp"

namespace mockturtle
{

struct xag_npn_resynthesis_params
{
  /*! \brief Be verbose. */
  bool verbose{false};
};

struct xag_npn_resynthesis_stats
{
  stopwatch<>::duration time_classes{0};
  stopwatch<>::duration time_db{0};

  uint32_t db_size;
  uint32_t covered_classes;

  void report() const
  {
    std::cout << fmt::format( "[i] build classes time = {:>5.2f} secs\n", to_seconds( time_classes ) );
    std::cout << fmt::format( "[i] build db time      = {:>5.2f} secs\n", to_seconds( time_db ) );
  }
};

enum class xag_npn_db_kind : uint32_t
{
  xag_incomplete = 0,
  xag_complete = 1,
  aig_complete = 2,
};

/*! \brief Resynthesis function based on pre-computed AIGs.
 *
 * This resynthesis function can be passed to ``cut_rewriting``.  It will
 * produce a network based on pre-computed XAGs with up to at most 4 variables.
 * Consequently, the nodes' fan-in sizes in the input network must not exceed
 * 4.
 *
   \verbatim embed:rst

   Example

   .. code-block:: c++

      const aig_network aig = ...;
      xag_npn_resynthesis<aig_network> resyn;
      aig = cut_rewriting( aig, resyn );

   .. note::

      The implementation of this algorithm was heavily inspired by the rewrite
      command in AIG.  It uses the same underlying database of subcircuits.
   \endverbatim
 */
template<class Ntk, class DatabaseNtk = xag_network, xag_npn_db_kind DBKind = xag_npn_db_kind::xag_incomplete>
class xag_npn_resynthesis
{
public:
  xag_npn_resynthesis( xag_npn_resynthesis_params const& ps = {}, xag_npn_resynthesis_stats* pst = nullptr )
      : ps( ps ),
        pst( pst ),
        _repr( 1u << 16u )
  {
    static_assert( is_network_type_v<Ntk>, "Ntk is not a network type" );
    static_assert( has_get_constant_v<Ntk>, "Ntk does not implement the get_constant method" );
    static_assert( has_create_and_v<Ntk>, "Ntk does not implement the create_and method" );
    static_assert( has_create_xor_v<Ntk>, "Ntk does not implement the create_xor method" );
    static_assert( has_create_not_v<Ntk>, "Ntk does not implement the create_not method" );

    static_assert( is_network_type_v<DatabaseNtk>, "DatabaseNtk is not a network type" );
    static_assert( has_get_node_v<DatabaseNtk>, "DatabaseNtk does not implement the get_node method" );
    static_assert( has_is_complemented_v<DatabaseNtk>, "DatabaseNtk does not implement the is_complemented method" );
    static_assert( has_is_xor_v<DatabaseNtk>, "DatabaseNtk does not implement the is_xor method" );
    static_assert( has_size_v<DatabaseNtk>, "DatabaseNtk does not implement the size method" );
    static_assert( has_create_pi_v<DatabaseNtk>, "DatabaseNtk does not implement the create_pi method" );
    static_assert( has_create_and_v<DatabaseNtk>, "DatabaseNtk does not implement the create_and method" );
    static_assert( has_create_xor_v<DatabaseNtk>, "DatabaseNtk does not implement the create_xor method" );
    static_assert( has_foreach_fanin_v<DatabaseNtk>, "DatabaseNtk does not implement the foreach_fanin method" );
    static_assert( has_foreach_node_v<DatabaseNtk>, "DatabaseNtk does not implement the foreach_node method" );
    static_assert( has_make_signal_v<DatabaseNtk>, "DatabaseNtk does not implement the make_signal method" );

    build_classes();
    build_db();
  }

  virtual ~xag_npn_resynthesis()
  {
    if ( ps.verbose )
    {
      st.report();
    }

    if ( pst )
    {
      *pst = st;
    }
  }

  template<typename LeavesIterator, typename Fn>
  void operator()( Ntk& ntk, kitty::dynamic_truth_table const& function, LeavesIterator begin, LeavesIterator end, Fn&& fn ) const
  {
    kitty::static_truth_table<4u> tt = kitty::extend_to<4u>( function );

    /* get representative of function */
    const auto [repr, phase, perm] = _repr[*tt.cbegin()];

    /* check if representative has circuits */
    const auto it = _repr_to_signal.find( repr );
    if ( it == _repr_to_signal.end() )
    {
      return;
    }

    std::vector<signal<Ntk>> pis( 4, ntk.get_constant( false ) );
    std::copy( begin, end, pis.begin() );

    std::unordered_map<node<DatabaseNtk>, signal<Ntk>> db_to_ntk;
    db_to_ntk.insert( {0, ntk.get_constant( false )} );
    for ( auto i = 0; i < 4; ++i )
    {
      db_to_ntk.insert( {i + 1, ( phase >> perm[i] & 1 ) ? ntk.create_not( pis[perm[i]] ) : pis[perm[i]]} );
    }

    for ( auto const& cand : it->second )
    {
      const auto f = copy_db_entry( ntk, _db.get_node( cand ), db_to_ntk );
      if ( !fn( _db.is_complemented( cand ) != ( phase >> 4 & 1 ) ? ntk.create_not( f ) : f ) )
      {
        return;
      }
    }
  }

private:
  signal<Ntk>
  copy_db_entry( Ntk& ntk, node<DatabaseNtk> const& n, std::unordered_map<node<DatabaseNtk>, signal<Ntk>>& db_to_ntk ) const
  {
    if ( const auto it = db_to_ntk.find( n ); it != db_to_ntk.end() )
    {
      return it->second;
    }

    std::array<signal<Ntk>, 2> fanin{};
    _db.foreach_fanin( n, [&]( auto const& f, auto i ) {
      const auto ntk_f = copy_db_entry( ntk, _db.get_node( f ), db_to_ntk );
      fanin[i] = _db.is_complemented( f ) ? ntk.create_not( ntk_f ) : ntk_f;
    } );

    const auto f = _db.is_xor( n ) ? ntk.create_xor( fanin[0], fanin[1] ) : ntk.create_and( fanin[0], fanin[1] );
    db_to_ntk.insert( {n, f} );
    return f;
  }

  void build_classes()
  {
    stopwatch t( st.time_classes );

    kitty::static_truth_table<4u> tt;
    do {
      _repr[*tt.cbegin()] = kitty::exact_npn_canonization( tt );
      kitty::next_inplace( tt );
    } while ( !kitty::is_const0( tt ) );
  }

  void build_db()
  {
    stopwatch t( st.time_db );

    if constexpr ( DBKind == xag_npn_db_kind::xag_incomplete )
    {
      decode( _db, xag_index_list{std::vector<uint32_t>{subgraphs, subgraphs + sizeof subgraphs / sizeof subgraphs[0]}} );
    }
    else if constexpr ( DBKind == xag_npn_db_kind::xag_complete )
    {
      decode( _db, xag_index_list{std::vector<uint32_t>{subgraphs_xag, subgraphs_xag + sizeof subgraphs_xag / sizeof subgraphs_xag[0]}} );
    }
    else if constexpr ( DBKind == xag_npn_db_kind::aig_complete )
    {
      decode( _db, xag_index_list{std::vector<uint32_t>{subgraphs_aig, subgraphs_aig + sizeof subgraphs_aig / sizeof subgraphs_aig[0]}} );
    }
    const auto sim_res = simulate_nodes<kitty::static_truth_table<4u>>( _db );

    _db.foreach_node( [&]( auto n ) {
      if ( std::get<0>( _repr[*sim_res[n].cbegin()] ) == sim_res[n] )
      {
        if ( _repr_to_signal.count( sim_res[n] ) == 0 )
        {
          _repr_to_signal.insert( {sim_res[n], {_db.make_signal( n )}} );
        }
        else
        {
          _repr_to_signal[sim_res[n]].push_back( _db.make_signal( n ) );
        }
      }
      else
      {
        const auto f = ~sim_res[n];
        if ( std::get<0>( _repr[*f.cbegin()] ) == f )
        {
          if ( _repr_to_signal.count( f ) == 0 )
          {
            _repr_to_signal.insert( {f, {!_db.make_signal( n )}} );
          }
          else
          {
            _repr_to_signal[f].push_back( !_db.make_signal( n ) );
          }
        }
      }
    } );

    st.db_size = _db.size();
    st.covered_classes = static_cast<uint32_t>( _repr_to_signal.size() );
  }

  xag_npn_resynthesis_params ps;
  xag_npn_resynthesis_stats st;
  xag_npn_resynthesis_stats* pst{nullptr};

  std::vector<std::tuple<kitty::static_truth_table<4u>, uint32_t, std::vector<uint8_t>>> _repr;
  std::unordered_map<kitty::static_truth_table<4u>, std::vector<signal<DatabaseNtk>>, kitty::hash<kitty::static_truth_table<4u>>> _repr_to_signal;

  DatabaseNtk _db;

  // clang-format off
  /* complete XAG database */
  inline static const uint32_t subgraphs_xag[] = { 38460932, 6, 4, 10, 8,
    8, 6, 3, 5, 16, 14, 3, 10, 20, 8, 22, 6, 2, 6, 4, 27, 8, 2, 30, 28,
    7, 8, 2, 35, 4, 37, 6, 9, 40, 2, 42, 38, 4, 2, 7, 46, 17, 49, 50, 8,
    4, 8, 54, 6, 3, 56, 5, 7, 60, 8, 62, 58, 3, 8, 66, 4, 8, 68, 4, 71,
    7, 69, 74, 72, 76, 2, 2, 4, 46, 8, 6, 83, 81, 85, 86, 8, 15, 83, 90,
    80, 4, 15, 2, 95, 96, 14, 98, 54, 4, 6, 3, 102, 8, 105, 106, 2, 108,
    60, 30, 4, 2, 112, 114, 6, 114, 8, 116, 118, 120, 112, 6, 54, 54, 2,
    5, 6, 128, 126, 125, 130, 6, 81, 8, 135, 136, 2, 138, 4, 2, 8, 4,
    142, 6, 145, 146, 4, 148, 2, 6, 2, 152, 4, 6, 31, 154, 157, 7, 55,
    3, 9, 162, 160, 46, 6, 8, 167, 166, 4, 47, 171, 169, 173, 8, 4, 47,
    153, 177, 179, 180, 152, 9, 167, 2, 177, 7, 187, 188, 8, 31, 177, 7,
    193, 194, 8, 7, 145, 198, 8, 6, 67, 11, 203, 9, 10, 206, 2, 208,
    204, 16, 6, 9, 212, 7, 81, 216, 214, 6, 8, 4, 152, 222, 162, 221,
    225, 166, 8, 81, 213, 16, 231, 9, 230, 234, 232, 9, 216, 10, 152,
    14, 241, 4, 31, 7, 163, 246, 8, 245, 249, 14, 46, 14, 2, 254, 4, 7,
    257, 2, 256, 14, 261, 259, 263, 8, 17, 135, 267, 2, 221, 4, 270,
    272, 6, 274, 8, 48, 8, 66, 28, 221, 281, 7, 9, 284, 2, 286, 4, 221,
    288, 3, 6, 267, 293, 2, 7, 8, 297, 298, 2, 298, 4, 300, 302, 304, 6,
    5, 153, 9, 309, 310, 60, 142, 4, 162, 6, 314, 317, 318, 8, 6, 80, 9,
    323, 5, 27, 326, 2, 328, 6, 8, 328, 331, 333, 9, 153, 14, 154, 337,
    339, 2, 15, 4, 343, 344, 2, 346, 6, 46, 284, 9, 223, 7, 154, 354,
    352, 2, 9, 7, 359, 360, 8, 11, 363, 364, 358, 296, 4, 7, 368, 368,
    2, 9, 373, 371, 375, 6, 176, 359, 379, 380, 4, 154, 221, 16, 8, 231,
    387, 8, 103, 390, 4, 2, 14, 394, 392, 8, 217, 17, 399, 400, 216,
    346, 220, 7, 31, 15, 407, 113, 409, 162, 4, 7, 413, 414, 2, 8, 415,
    416, 419, 216, 8, 10, 2, 7, 424, 2, 11, 9, 429, 430, 426, 7, 113,
    434, 8, 4, 9, 6, 439, 154, 441, 442, 8, 80, 6, 47, 447, 8, 449, 450,
    446, 5, 9, 253, 455, 4, 163, 3, 7, 460, 458, 221, 463, 9, 155, 466,
    354, 3, 11, 470, 8, 55, 473, 5, 284, 4, 285, 478, 2, 221, 480, 477,
    483, 15, 461, 14, 4, 488, 2, 487, 491, 2, 63, 494, 60, 255, 489,
    221, 499, 358, 6, 5, 503, 504, 8, 8, 152, 3, 509, 510, 176, 309,
    512, 498, 6, 2, 10, 518, 6, 520, 8, 10, 521, 522, 525, 14, 223, 2,
    103, 9, 531, 532, 60, 8, 61, 47, 537, 11, 14, 163, 541, 4, 14, 544,
    6, 10, 461, 55, 549, 544, 360, 6, 55, 554, 4, 14, 176, 11, 221, 163,
    560, 562, 8, 14, 67, 566, 326, 26, 4, 9, 570, 572, 60, 9, 254, 14,
    257, 577, 579, 8, 47, 11, 583, 584, 2, 7, 176, 176, 2, 9, 590, 589,
    593, 102, 8, 2, 596, 598, 4, 600, 6, 9, 103, 438, 6, 4, 7, 359, 609,
    610, 606, 6, 571, 8, 615, 616, 570, 11, 30, 620, 6, 622, 2, 3, 4, 8,
    609, 627, 629, 630, 6, 5, 293, 8, 635, 2, 637, 638, 634, 9, 425,
    642, 60, 358, 4, 646, 6, 8, 646, 649, 651, 30, 176, 5, 655, 656, 30,
    7, 658, 660, 654, 27, 537, 608, 8, 359, 667, 668, 6, 3, 221, 5, 672,
    285, 675, 9, 152, 61, 679, 14, 583, 14, 30, 176, 684, 28, 2, 9, 689,
    61, 163, 8, 10, 103, 695, 27, 425, 14, 699, 394, 6, 545, 703, 5,
    246, 706, 8, 103, 709, 6, 47, 9, 713, 162, 60, 390, 6, 718, 4, 6,
    359, 5, 723, 724, 8, 7, 16, 728, 8, 674, 8, 14, 47, 734, 6, 3, 176,
    6, 738, 8, 739, 741, 743, 471, 537, 746, 60, 470, 6, 11, 751, 473,
    753, 293, 387, 30, 537, 8, 247, 4, 761, 762, 246, 3, 14, 8, 767, 5,
    14, 770, 766, 769, 773, 4, 153, 3, 777, 778, 4, 8, 780, 776, 6, 784,
    782, 21, 267, 5, 285, 2, 791, 792, 284, 221, 795, 143, 771, 798, 2,
    152, 771, 221, 803, 46, 607, 806, 8, 766, 8, 488, 811, 7, 387, 9,
    47, 816, 814, 102, 2, 596, 821, 822, 60, 387, 713, 5, 30, 8, 829,
    30, 6, 832, 4, 831, 834, 230, 8, 143, 785, 387, 447, 30, 61, 293,
    845, 846, 2, 267, 447, 7, 177, 163, 853, 854, 6, 240, 8, 60, 2, 63,
    860, 55, 620, 3, 285, 5, 867, 868, 2, 221, 871, 14, 654, 874, 8, 4,
    143, 878, 2, 878, 6, 881, 883, 884, 8, 267, 713, 10, 30, 176, 424,
    891, 893, 163, 556, 5, 766, 898, 8, 9, 240, 9, 179, 102, 30, 537,
    906, 46, 441, 910, 8, 460, 4, 7, 915, 914, 2, 9, 918, 917, 921, 8,
    471, 103, 925, 212, 4, 267, 928, 167, 387, 292, 4, 157, 935, 936,
    30, 46, 221, 394, 4, 11, 943, 16, 284, 296, 60, 15, 297, 949, 951,
    176, 6, 743, 954, 15, 163, 11, 959, 3, 60, 962, 604, 9, 17, 966,
    216, 588, 162, 63, 820, 972, 60, 394, 8, 4, 977, 978, 14, 284, 673,
    982, 674, 8, 323, 986, 154, 766, 4, 221, 991, 5, 470, 994, 206, 6,
    187, 4, 67, 1000, 998, 6, 17, 9, 1005, 9, 820, 61, 1009, 386, 6, 81,
    1013, 1005, 1014, 15, 31, 47, 1019, 1020, 6, 2, 61, 1024, 4, 1026,
    6, 9, 1029, 152, 8, 6, 1032, 152, 439, 1036, 4, 1035, 1038, 2, 102,
    9, 1043, 1044, 60, 7, 591, 1048, 8, 739, 1051, 6, 155, 3, 155, 1056,
    8, 1055, 1059, 4, 359, 1062, 2, 7, 1064, 1066, 8, 503, 647, 1070, 8,
    61, 143, 1074, 2, 518, 4, 9, 1079, 460, 8, 47, 1083, 674, 284, 3,
    177, 1088, 6, 1032, 1091, 285, 673, 4, 1095, 1096, 672, 28, 8, 1100,
    6, 689, 1102, 9, 519, 1106, 60, 9, 60, 9, 739, 1112, 188, 155, 267,
    7, 17, 1118, 4, 9, 1121, 503, 591, 1124, 8, 9, 213, 296, 8, 4, 1131,
    359, 1133, 1134, 6, 9, 81, 424, 1138, 634, 2, 221, 1143, 530, 6, 9,
    1146, 61, 1149, 6, 46, 9, 1153, 81, 1154, 187, 424, 1158, 8, 9, 61,
    1162, 6, 46, 1165, 21, 387, 2, 853, 1170, 4, 221, 1173, 2, 455,
    1176, 10, 221, 1178, 13, 18, 24, 32, 45, 52, 65, 79, 89, 93, 101,
    110, 123, 132, 141, 150, 158, 164, 174, 182, 184, 191, 197, 201,
    211, 218, 226, 228, 236, 238, 242, 250, 252, 265, 268, 276, 279,
    282, 290, 294, 307, 312, 321, 324, 334, 341, 348, 350, 356, 366,
    377, 382, 384, 388, 397, 402, 404, 410, 420, 338, 423, 432, 437, 14,
    445, 452, 457, 464, 468, 474, 485, 492, 496, 500, 507, 514, 517,
    526, 528, 534, 63, 538, 543, 547, 550, 552, 557, 558, 565, 568, 574,
    581, 587, 595, 602, 604, 612, 206, 618, 624, 633, 640, 644, 652,
    662, 664, 671, 677, 681, 682, 686, 690, 693, 696, 700, 704, 710,
    714, 716, 720, 727, 731, 9, 733, 737, 744, 748, 754, 756, 758, 764,
    774, 787, 788, 796, 801, 804, 809, 812, 818, 824, 826, 836, 839,
    840, 842, 848, 850, 856, 859, 862, 864, 872, 877, 884, 887, 888,
    895, 897, 901, 902, 904, 908, 913, 923, 926, 930, 932, 938, 940,
    944, 946, 952, 956, 960, 964, 968, 970, 974, 980, 984, 989, 992,
    996, 1003, 1006, 1011, 1016, 1023, 1030, 1040, 1046, 1052, 1060,
    1069, 1073, 1077, 1080, 1084, 1086, 1092, 1098, 1104, 1108, 284,
    1110, 1114, 8, 1116, 1122, 1127, 1128, 1136, 1140, 1144, 1151, 1156,
    1161, 1166, 1168, 1174, 1180 };

  /* complete AIG database */
  inline static const uint32_t subgraphs_aig [] = { 52223492, 4, 7, 5,
    6, 11, 13, 8, 14, 9, 15, 17, 19, 3, 5, 6, 9, 7, 8, 25, 27, 23, 29,
    22, 28, 31, 33, 3, 4, 2, 6, 37, 39, 8, 40, 9, 41, 43, 45, 2, 5, 2,
    7, 4, 51, 49, 53, 8, 55, 9, 54, 57, 59, 2, 26, 25, 63, 2, 63, 5,
    67, 65, 68, 64, 69, 71, 73, 2, 4, 6, 23, 77, 79, 8, 80, 9, 81, 83,
    85, 5, 39, 8, 88, 2, 8, 6, 39, 93, 95, 89, 96, 91, 99, 4, 8, 2,
    103, 13, 104, 13, 27, 3, 109, 107, 111, 8, 76, 6, 22, 77, 117, 27,
    118, 115, 121, 7, 9, 22, 125, 6, 8, 23, 129, 76, 125, 130, 133,
    127, 135, 5, 8, 3, 139, 93, 141, 4, 141, 7, 145, 142, 146, 143,
    147, 149, 151, 5, 7, 8, 155, 9, 154, 157, 159, 2, 161, 4, 6, 161,
    165, 3, 167, 163, 169, 2, 9, 4, 173, 3, 8, 7, 176, 174, 179, 39,
    179, 5, 183, 181, 185, 4, 9, 155, 189, 2, 190, 165, 190, 3, 195,
    193, 197, 23, 77, 6, 77, 8, 203, 200, 205, 201, 204, 207, 209, 7,
    23, 77, 212, 9, 76, 23, 217, 6, 219, 215, 221, 23, 25, 77, 129,
    224, 226, 225, 227, 229, 231, 3, 9, 7, 103, 235, 236, 234, 237,
    239, 241, 23, 115, 7, 245, 8, 23, 77, 249, 6, 251, 247, 253, 23,
    125, 227, 257, 226, 256, 259, 261, 6, 200, 7, 201, 265, 267, 9,
    269, 49, 177, 7, 273, 25, 275, 7, 173, 4, 177, 278, 281, 25, 283,
    7, 77, 8, 287, 125, 289, 9, 165, 155, 293, 3, 295, 8, 164, 2, 294,
    299, 301, 297, 302, 4, 50, 5, 234, 307, 309, 129, 310, 11, 23,
    177, 315, 129, 317, 37, 49, 6, 320, 7, 321, 323, 325, 8, 326, 9,
    327, 329, 331, 9, 77, 7, 334, 23, 337, 129, 339, 9, 286, 26, 77,
    9, 23, 6, 346, 345, 349, 4, 234, 7, 139, 2, 354, 353, 357, 129,
    358, 77, 256, 129, 362, 2, 124, 4, 366, 3, 125, 4, 371, 367, 373,
    129, 374, 369, 377, 203, 249, 6, 76, 343, 383, 289, 384, 8, 325,
    9, 324, 389, 391, 8, 11, 51, 394, 51, 235, 4, 399, 397, 401, 367,
    371, 4, 405, 5, 404, 407, 409, 129, 411, 3, 6, 249, 415, 5, 176,
    4, 129, 2, 420, 419, 423, 6, 424, 7, 425, 427, 429, 5, 9, 2, 432,
    157, 435, 3, 7, 7, 439, 2, 441, 4, 443, 439, 444, 8, 445, 441,
    448, 447, 451, 9, 383, 24, 37, 325, 457, 9, 37, 11, 461, 50, 463,
    51, 462, 465, 467, 88, 439, 173, 439, 4, 473, 471, 475, 50, 139,
    139, 189, 3, 481, 479, 483, 129, 484, 155, 235, 293, 488, 292,
    489, 491, 493, 6, 321, 9, 51, 320, 499, 497, 501, 5, 172, 129,
    505, 4, 278, 506, 509, 7, 200, 24, 201, 513, 515, 7, 22, 347, 519,
    337, 521, 5, 399, 398, 420, 525, 527, 22, 286, 287, 346, 531, 533,
    3, 129, 4, 536, 2, 128, 4, 125, 541, 543, 537, 544, 539, 547, 8,
    77, 212, 551, 9, 201, 213, 555, 553, 557, 154, 370, 9, 371, 155,
    562, 561, 565, 24, 320, 26, 321, 569, 571, 8, 286, 9, 287, 575,
    577, 2, 542, 3, 543, 7, 583, 4, 543, 9, 587, 585, 589, 581, 591,
    25, 325, 125, 129, 9, 212, 8, 213, 77, 601, 598, 602, 599, 603,
    605, 607, 7, 93, 4, 235, 611, 612, 610, 613, 615, 617, 129, 618,
    5, 370, 7, 623, 8, 625, 373, 627, 3, 236, 129, 631, 77, 632, 125,
    201, 129, 637, 3, 154, 8, 641, 155, 165, 234, 645, 643, 647, 5,
    124, 3, 651, 542, 653, 543, 652, 129, 657, 655, 658, 4, 370, 5,
    367, 371, 664, 663, 667, 129, 669, 173, 641, 3, 124, 5, 674, 581,
    677, 129, 678, 9, 49, 155, 682, 154, 683, 685, 687, 248, 286, 22,
    287, 76, 249, 693, 695, 691, 696, 9, 22, 265, 701, 115, 702, 334,
    415, 157, 707, 6, 460, 4, 37, 7, 713, 8, 714, 711, 717, 2, 165, 9,
    721, 155, 722, 154, 723, 725, 727, 8, 154, 9, 155, 731, 733, 5,
    129, 2, 736, 173, 737, 739, 741, 165, 172, 157, 745, 13, 103, 51,
    188, 155, 751, 9, 50, 748, 755, 4, 24, 155, 759, 7, 138, 759, 763,
    2, 645, 9, 767, 731, 769, 8, 720, 6, 721, 9, 774, 773, 777, 4,
    778, 5, 779, 781, 783, 12, 173, 6, 172, 9, 789, 4, 791, 787, 793,
    2, 237, 4, 796, 129, 799, 631, 800, 125, 219, 7, 218, 77, 806,
    805, 809, 6, 235, 9, 813, 8, 812, 5, 817, 815, 819, 309, 821, 92,
    154, 3, 164, 93, 827, 155, 828, 825, 831, 188, 789, 279, 789, 5,
    837, 835, 839, 9, 644, 9, 39, 5, 844, 737, 845, 847, 849, 3, 138,
    25, 51, 2, 139, 5, 856, 855, 859, 853, 861, 77, 433, 7, 865, 9,
    865, 6, 869, 867, 871, 5, 439, 175, 875, 234, 293, 235, 295, 879,
    881, 188, 836, 839, 885, 27, 77, 25, 201, 889, 891, 888, 890, 893,
    895, 235, 237, 7, 234, 5, 900, 103, 903, 813, 904, 5, 536, 125,
    909, 6, 234, 9, 235, 4, 915, 7, 917, 913, 919, 8, 439, 237, 922,
    236, 923, 925, 927, 4, 172, 6, 930, 7, 852, 933, 935, 53, 682,
    157, 165, 6, 37, 8, 321, 943, 945, 129, 947, 5, 23, 6, 951, 249,
    953, 2, 154, 9, 957, 165, 958, 731, 961, 9, 323, 154, 234, 489,
    967, 160, 165, 5, 415, 9, 972, 7, 972, 8, 977, 975, 979, 8, 518,
    9, 519, 983, 985, 22, 26, 347, 989, 8, 320, 497, 993, 643, 827, 3,
    165, 2, 155, 999, 1001, 157, 1003, 3, 433, 154, 1007, 6, 1006, 9,
    1011, 155, 1013, 1009, 1015, 3, 11, 8, 1019, 27, 1018, 1021, 1023,
    8, 640, 173, 1027, 7, 235, 5, 1030, 4, 1031, 9, 1034, 1033, 1037,
    4, 537, 6, 1041, 9, 1043, 909, 1045, 6, 177, 5, 1049, 179, 1050,
    173, 179, 4, 1055, 1053, 1057, 9, 999, 5, 998, 7, 1062, 1061,
    1065, 129, 675, 581, 1068, 3, 13, 8, 1072, 5, 1074, 2, 12, 9,
    1073, 1079, 1080, 1077, 1083, 7, 857, 4, 857, 6, 1089, 9, 1090,
    1087, 1093, 324, 461, 325, 460, 1097, 1099, 93, 125, 415, 1102, 5,
    1105, 543, 1107, 5, 93, 7, 1110, 6, 1111, 2, 1114, 3, 1115, 1117,
    1119, 9, 1121, 1113, 1123, 8, 998, 2, 164, 9, 1128, 155, 1131,
    1126, 1132, 1127, 1133, 1135, 1137, 6, 335, 249, 701, 1141, 1142,
    77, 701, 7, 1147, 6, 1146, 249, 1151, 1149, 1152, 23, 579, 22,
    578, 1157, 1159, 77, 155, 93, 1163, 4, 415, 1031, 1167, 4, 1030,
    93, 1171, 1169, 1172, 9, 415, 155, 1176, 641, 1179, 287, 383, 249,
    1183, 125, 488, 124, 489, 1187, 1189, 5, 414, 2, 10, 1193, 1195,
    8, 1197, 9, 1196, 1199, 1201, 155, 172, 154, 176, 1205, 1207, 9,
    766, 730, 767, 1211, 1213, 875, 1007, 129, 1217, 455, 519, 23,
    165, 6, 173, 1223, 1225, 383, 641, 9, 1229, 643, 1231, 6, 201,
    249, 1235, 93, 415, 6, 415, 5, 1241, 1238, 1243, 8, 1242, 1239,
    1246, 1245, 1249, 155, 723, 9, 973, 53, 1254, 454, 519, 2, 293, 3,
    292, 157, 1263, 1261, 1264, 23, 1001, 9, 1268, 7, 1268, 8, 1273,
    1271, 1275, 5, 371, 37, 1279, 129, 1281, 165, 643, 49, 103, 7,
    1286, 6, 1287, 9, 1290, 1289, 1293, 7, 335, 265, 1297, 249, 1299,
    1050, 1054, 1057, 1303, 129, 200, 155, 1129, 93, 1309, 22, 124, 3,
    102, 49, 1315, 7, 1317, 25, 1319, 9, 645, 643, 1323, 9, 164, 154,
    173, 1327, 1329, 9, 640, 1284, 1333, 286, 347, 533, 1337, 27, 235,
    10, 1341, 11, 1340, 1343, 1345, 2, 759, 9, 1348, 3, 761, 1351,
    1353, 461, 714, 460, 715, 1357, 1359, 9, 537, 7, 1362, 909, 1365,
    23, 423, 596, 1368, 597, 1369, 1371, 1373, 663, 1279, 129, 1377,
    641, 733, 165, 1381, 3, 189, 7, 1385, 4, 1386, 9, 1385, 6, 1391,
    1389, 1393, 9, 79, 155, 1061, 1129, 1399, 226, 257, 1313, 1402, 8,
    22, 286, 1407, 221, 1409, 9, 1129, 155, 998, 1412, 1415, 4, 439,
    173, 1418, 439, 1049, 5, 1423, 1421, 1425, 160, 1129, 7, 37, 9,
    36, 1431, 1433, 49, 1435, 129, 1437, 5, 51, 1177, 1441, 1176,
    1440, 129, 1445, 1443, 1446, 9, 213, 212, 550, 1451, 1453, 157,
    1129, 3, 158, 1456, 1459, 3, 155, 2, 733, 1463, 1465, 39, 460,
    235, 875, 234, 874, 1471, 1473, 103, 1475, 125, 908, 124, 909,
    1479, 1481, 675, 911, 2, 189, 51, 737, 1487, 1489, 4, 124, 909,
    1493, 675, 1495, 165, 1463, 9, 1499, 731, 1501, 6, 461, 3, 460, 5,
    1507, 1430, 1509, 1505, 1511, 2, 188, 23, 1515, 7, 1517, 6, 1516,
    9, 1520, 1519, 1523, 292, 957, 5, 438, 581, 1529, 129, 1530, 79,
    519, 9, 1534, 7, 347, 77, 1538, 349, 1541, 80, 984, 226, 519, 77,
    415, 9, 1549, 155, 1551, 79, 334, 8, 644, 165, 1557, 2, 1559,
    1323, 1557, 3, 1562, 1561, 1565, 129, 373, 23, 1568, 6, 433, 3,
    1573, 8, 1575, 5, 433, 1574, 1579, 1577, 1581, 9, 13, 2, 1585, 8,
    12, 5, 1589, 3, 1591, 1587, 1593, 8, 48, 1430, 1597, 1505, 1599,
    20, 35, 47, 60, 74, 87, 101, 113, 122, 137, 152, 170, 186, 198,
    210, 223, 233, 243, 254, 263, 270, 277, 285, 290, 304, 312, 318,
    333, 340, 342, 351, 360, 364, 379, 380, 386, 392, 402, 412, 416,
    430, 436, 452, 454, 459, 468, 477, 390, 486, 494, 502, 510, 517,
    522, 529, 535, 549, 558, 567, 573, 579, 592, 595, 596, 608, 620,
    628, 634, 638, 648, 660, 670, 673, 680, 689, 699, 704, 708, 719,
    729, 735, 742, 746, 748, 753, 756, 761, 765, 771, 784, 794, 802,
    811, 822, 833, 292, 841, 842, 850, 863, 872, 876, 883, 887, 897,
    899, 906, 911, 921, 928, 937, 938, 489, 940, 948, 954, 963, 964,
    968, 970, 980, 987, 9, 991, 994, 996, 1004, 1016, 1024, 1029,
    1039, 1047, 1059, 1067, 1070, 1085, 1095, 1101, 1108, 1125, 1139,
    1144, 1154, 1161, 1164, 1174, 1181, 1184, 1190, 1203, 1209, 1215,
    1218, 1221, 1226, 1232, 1236, 1251, 1253, 521, 1256, 1258, 1266,
    1276, 1282, 1284, 1295, 1300, 1305, 1306, 1310, 1312, 1321, 1324,
    1331, 1334, 1339, 1346, 1355, 1361, 1367, 1375, 1378, 1382, 1394,
    1396, 1400, 1404, 1411, 1416, 1426, 1428, 1438, 1448, 1455, 1460,
    1466, 1468, 1476, 1483, 1484, 1490, 1496, 1503, 124, 158, 1512, 8,
    1525, 1526, 1532, 1536, 1543, 1544, 1546, 1553, 1554, 1566, 1570,
    1582, 1594, 1600 };

  /* incomplete XAG database */
  inline static const uint32_t subgraphs[] = {1780 << 16 | 0 << 8 | 4,
      2, 4, 2, 5, 3, 4, 3, 5, 4, 2, 2, 6, 2, 7, 3, 6, 3, 7, 6, 2, 4, 6,
      4, 7, 5, 6, 5, 7, 6, 4, 2, 8, 2, 9, 3, 8, 3, 9, 8, 2, 4, 8,
      4, 9, 5, 8, 5, 9, 8, 4, 6, 8, 6, 9, 7, 8, 7, 9, 8, 6, 5, 11,
      6, 10, 6, 11, 7, 10, 7, 11, 10, 6, 8, 10, 8, 11, 9, 10, 9, 11, 10, 8,
      6, 12, 6, 13, 7, 12, 7, 13, 12, 6, 9, 12, 9, 13, 12, 8, 5, 15, 6, 14,
      6, 15, 7, 14, 7, 15, 14, 6, 8, 14, 8, 15, 9, 14, 9, 15, 14, 8, 6, 16,
      6, 17, 7, 16, 7, 17, 16, 6, 8, 16, 8, 17, 9, 16, 9, 17, 16, 8, 6, 18,
      6, 19, 7, 18, 7, 19, 18, 6, 8, 19, 9, 18, 9, 19, 18, 8, 4, 20, 4, 21,
      5, 20, 7, 21, 8, 20, 9, 21, 20, 8, 11, 21, 20, 10, 15, 21, 20, 14, 17, 21,
      19, 21, 4, 22, 4, 23, 5, 22, 9, 22, 9, 23, 22, 8, 22, 12, 15, 23, 17, 23,
      18, 23, 4, 24, 7, 25, 9, 25, 24, 8, 11, 25, 13, 25, 15, 25, 24, 14, 19, 25,
      4, 26, 4, 27, 5, 26, 5, 27, 26, 4, 8, 27, 9, 26, 9, 27, 26, 8, 11, 27,
      13, 27, 17, 27, 26, 16, 19, 27, 4, 28, 28, 4, 9, 28, 9, 29, 28, 8, 11, 28,
      11, 29, 13, 29, 17, 29, 18, 29, 19, 28, 19, 29, 2, 30, 2, 31, 3, 30, 5, 31,
      7, 31, 8, 30, 8, 31, 9, 30, 9, 31, 30, 8, 13, 31, 17, 31, 19, 31, 23, 31,
      27, 31, 29, 31, 2, 32, 2, 33, 5, 33, 32, 6, 8, 33, 32, 8, 13, 33, 17, 33,
      21, 33, 25, 33, 27, 33, 28, 33, 32, 28, 2, 34, 3, 35, 34, 4, 7, 35, 34, 8,
      11, 35, 15, 35, 19, 35, 34, 18, 23, 35, 27, 35, 33, 35, 2, 36, 2, 37, 3, 36,
      3, 37, 36, 2, 8, 36, 8, 37, 9, 36, 9, 37, 36, 8, 11, 37, 15, 37, 17, 37,
      18, 37, 19, 37, 21, 37, 25, 37, 27, 37, 29, 37, 2, 38, 3, 38, 38, 2, 8, 38,
      8, 39, 9, 38, 9, 39, 38, 8, 11, 38, 11, 39, 15, 38, 15, 39, 17, 39, 18, 38,
      19, 38, 19, 39, 21, 39, 23, 38, 25, 39, 27, 38, 27, 39, 28, 38, 29, 38, 29, 39,
      4, 40, 4, 41, 6, 40, 9, 41, 13, 41, 15, 41, 19, 41, 23, 41, 25, 41, 29, 41,
      31, 41, 33, 41, 35, 41, 36, 41, 37, 41, 40, 36, 39, 41, 4, 42, 4, 43, 5, 42,
      6, 43, 7, 42, 17, 43, 27, 43, 30, 43, 31, 42, 31, 43, 32, 43, 33, 42, 42, 32,
      36, 43, 37, 42, 37, 43, 42, 36, 39, 42, 39, 43, 42, 38, 7, 45, 9, 45, 11, 45,
      21, 45, 31, 45, 44, 32, 36, 44, 36, 45, 39, 45, 44, 38, 4, 46, 4, 47, 5, 46,
      6, 47, 7, 46, 46, 6, 13, 47, 19, 47, 23, 47, 31, 46, 46, 30, 32, 47, 33, 47,
      34, 47, 35, 47, 36, 46, 36, 47, 37, 46, 37, 47, 46, 36, 38, 47, 39, 47, 4, 49,
      48, 4, 6, 49, 48, 6, 15, 48, 19, 48, 19, 49, 25, 48, 28, 49, 29, 48, 29, 49,
      31, 49, 33, 48, 35, 48, 36, 49, 39, 48, 48, 38, 2, 50, 2, 51, 6, 50, 7, 51,
      9, 51, 13, 51, 19, 51, 21, 51, 23, 51, 25, 51, 26, 51, 50, 26, 31, 51, 35, 51,
      39, 51, 47, 51, 48, 51, 2, 53, 3, 52, 6, 52, 6, 53, 17, 53, 22, 52, 23, 52,
      23, 53, 26, 53, 27, 53, 37, 53, 45, 53, 3, 55, 7, 55, 9, 55, 11, 55, 21, 55,
      22, 55, 23, 55, 26, 54, 26, 55, 31, 55, 43, 55, 53, 55, 2, 56, 3, 56, 6, 57,
      7, 56, 56, 6, 11, 57, 15, 57, 19, 57, 21, 56, 56, 20, 23, 57, 24, 57, 25, 56,
      25, 57, 26, 56, 27, 56, 27, 57, 56, 26, 33, 57, 41, 57, 2, 59, 3, 59, 58, 2,
      6, 59, 7, 58, 7, 59, 58, 6, 13, 59, 17, 59, 19, 59, 58, 20, 25, 59, 26, 59,
      27, 59, 58, 28, 35, 58, 58, 34, 38, 58, 38, 59, 39, 58, 43, 59, 47, 59, 2, 60,
      4, 60, 4, 61, 5, 61, 60, 4, 9, 61, 10, 61, 11, 61, 13, 61, 15, 61, 16, 61,
      17, 61, 18, 61, 19, 61, 23, 61, 27, 61, 33, 61, 39, 61, 43, 61, 47, 61, 48, 61,
      60, 52, 57, 61, 58, 61, 2, 63, 4, 62, 4, 63, 12, 63, 13, 62, 17, 63, 19, 63,
      27, 63, 37, 63, 45, 63, 55, 63, 3, 65, 5, 65, 9, 65, 11, 65, 16, 64, 16, 65,
      18, 65, 21, 65, 31, 65, 43, 65, 53, 65, 57, 65, 63, 65, 2, 66, 2, 67, 3, 66,
      3, 67, 66, 2, 4, 67, 5, 66, 66, 4, 10, 67, 11, 66, 66, 10, 13, 67, 14, 67,
      15, 67, 16, 66, 17, 66, 17, 67, 66, 16, 18, 66, 19, 66, 19, 67, 66, 18, 25, 67,
      35, 67, 41, 67, 51, 67, 57, 67, 3, 69, 68, 2, 4, 68, 4, 69, 5, 68, 68, 4,
      11, 69, 16, 69, 17, 68, 17, 69, 68, 16, 18, 68, 18, 69, 68, 18, 23, 69, 27, 69,
      68, 32, 37, 69, 39, 68, 43, 69, 47, 69, 57, 69, 58, 68, 70, 68, 9, 73, 37, 73,
      41, 73, 45, 73, 51, 73, 55, 73, 61, 73, 65, 73, 74, 2, 74, 4, 74, 16, 74, 18,
      33, 75, 41, 75, 74, 46, 48, 75, 51, 75, 58, 75, 67, 75, 8, 77, 9, 77, 76, 8,
      17, 77, 35, 77, 51, 77, 61, 77, 68, 77, 69, 77, 76, 68, 78, 2, 8, 79, 9, 78,
      9, 79, 78, 8, 17, 79, 78, 16, 31, 79, 63, 79, 9, 80, 17, 80, 48, 81, 51, 81,
      6, 83, 7, 83, 17, 83, 68, 83, 75, 83, 7, 85, 21, 85, 6, 87, 17, 87, 27, 87,
      37, 87, 61, 87, 65, 87, 67, 87, 69, 87, 6, 89, 7, 88, 88, 6, 23, 89, 88, 22,
      25, 88, 33, 89, 61, 89, 90, 74, 9, 93, 15, 93, 9, 94, 9, 95, 15, 95, 94, 14,
      23, 95, 9, 97, 25, 97, 31, 97, 51, 97, 9, 99, 98, 14, 21, 99, 35, 99, 45, 98,
      47, 99, 98, 46, 69, 99, 7, 103, 33, 103, 35, 103, 37, 103, 39, 103, 51, 103, 61, 103,
      6, 105, 21, 104, 27, 104, 27, 105, 104, 26, 31, 104, 37, 105, 104, 36, 55, 105, 65, 105,
      69, 105, 108, 68, 112, 4, 13, 113, 33, 113, 58, 112, 61, 115, 97, 115, 103, 115, 116, 4,
      8, 117, 9, 117, 57, 117, 116, 56, 63, 117, 13, 118, 13, 119, 55, 119, 61, 121, 98, 121,
      122, 2, 23, 125, 61, 125, 6, 127, 126, 6, 21, 126, 27, 127, 37, 126, 37, 127, 126, 36,
      65, 127, 77, 127, 126, 78, 128, 20, 77, 131, 9, 133, 11, 133, 132, 10, 79, 133, 88, 133,
      8, 135, 9, 134, 9, 135, 134, 8, 11, 135, 43, 135, 134, 42, 53, 135, 61, 135, 63, 135,
      73, 135, 87, 135, 134, 86, 134, 88, 136, 4, 136, 6, 9, 136, 9, 137, 136, 8, 47, 137,
      53, 136, 55, 136, 57, 137, 61, 137, 63, 137, 69, 137, 136, 68, 75, 137, 89, 137, 105, 137,
      127, 137, 9, 139, 138, 8, 11, 138, 11, 139, 88, 139, 21, 141, 31, 141, 43, 141, 63, 141,
      73, 141, 133, 141, 7, 143, 25, 143, 27, 143, 35, 143, 39, 143, 47, 143, 67, 143, 75, 143,
      78, 143, 79, 143, 95, 143, 97, 143, 101, 143, 131, 143, 6, 145, 7, 144, 7, 145, 144, 6,
      73, 145, 144, 78, 143, 145, 146, 4, 7, 146, 146, 6, 27, 146, 27, 147, 69, 147, 135, 147,
      7, 148, 148, 6, 25, 149, 61, 149, 81, 149, 101, 149, 131, 149, 150, 90, 9, 153, 143, 153,
      9, 154, 154, 62, 61, 157, 68, 157, 156, 68, 9, 159, 158, 8, 61, 158, 68, 158, 83, 158,
      143, 159, 149, 159, 68, 161, 151, 161, 158, 161, 7, 162, 21, 164, 28, 164, 31, 164, 38, 164,
      164, 134, 166, 6, 68, 167, 166, 72, 158, 167, 9, 169, 168, 166, 170, 48, 174, 58, 158, 177,
      15, 178, 19, 178, 180, 14, 9, 186, 188, 8, 9, 192, 192, 68, 68, 195, 194, 68, 104, 197,
      202, 78, 9, 211, 210, 8, 216, 58, 41, 226, 48, 226, 143, 229, 149, 229, 41, 230, 51, 230,
      61, 231, 178, 235, 9, 236, 236, 42, 236, 86, 236, 164, 238, 58, 178, 241, 19, 243, 159, 243,
      186, 243, 192, 243, 211, 243, 213, 243, 229, 243, 5, 244, 19, 249, 149, 249, 159, 249, 186, 249,
      192, 249, 211, 249, 143, 257, 149, 257, 243, 257, 249, 257, 68, 261, 260, 180, 9, 263, 262, 8,
      61, 262, 68, 262, 83, 262, 143, 263, 149, 263, 177, 262, 243, 263, 249, 263, 19, 264, 264, 36,
      38, 264, 268, 4, 143, 271, 149, 271, 272, 58, 9, 280, 9, 283, 41, 282, 48, 282, 51, 282,
      58, 282, 61, 282, 68, 282, 282, 166, 9, 285, 286, 58, 290, 68, 292, 58, 158, 295, 262, 295,
      296, 38, 19, 300, 300, 36, 97, 300, 300, 134, 199, 300, 223, 300, 300, 236, 252, 300, 302, 36,
      302, 222, 246, 304, 9, 308, 308, 68, 243, 308, 249, 308, 310, 58, 104, 312, 314, 58, 68, 317,
      316, 68, 126, 319, 320, 68, 322, 8, 326, 6, 326, 210, 330, 204, 246, 331, 330, 248, 332, 48,
      126, 335, 334, 128, 143, 339, 149, 339, 41, 341, 48, 341, 346, 8, 348, 58, 350, 4, 350, 252,
      178, 353, 352, 180, 41, 354, 41, 356, 51, 356, 61, 357, 41, 359, 48, 359, 104, 361, 360, 106,
      362, 106, 364, 8, 300, 367, 300, 369, 9, 370, 370, 42, 370, 86, 370, 300, 41, 373, 48, 373,
      372, 48, 41, 374, 48, 374, 300, 375, 376, 104, 376, 178, 376, 264, 376, 300, 19, 379, 21, 379,
      31, 379, 48, 379, 101, 379, 103, 379, 159, 379, 182, 379, 185, 379, 192, 379, 207, 379, 263, 379,
      267, 379, 271, 379, 277, 379, 301, 379, 308, 379, 339, 379, 369, 379, 374, 379, 3, 380, 379, 381,
      186, 382, 211, 382, 19, 385, 31, 385, 48, 385, 93, 385, 101, 385, 103, 385, 153, 385, 159, 385,
      173, 385, 185, 385, 192, 385, 207, 385, 384, 210, 384, 254, 263, 385, 267, 385, 271, 385, 279, 385,
      308, 385, 339, 385, 343, 385, 374, 385, 41, 387, 178, 388, 388, 220, 390, 248, 243, 393, 126, 396,
      398, 128, 400, 8, 400, 148, 379, 403, 385, 403, 404, 302, 379, 405, 385, 405, 143, 407, 149, 407,
      243, 407, 249, 407, 9, 409, 408, 8, 61, 408, 68, 408, 83, 408, 143, 409, 149, 409, 177, 408,
      243, 409, 249, 409, 295, 408, 379, 409, 385, 409, 19, 414, 28, 414, 414, 134, 414, 236, 414, 370,
      413, 415, 418, 2, 143, 418, 243, 418, 422, 48, 51, 425, 41, 426, 48, 426, 9, 429, 379, 429,
      411, 429, 418, 429, 385, 431, 9, 432, 9, 435, 41, 434, 48, 434, 51, 434, 58, 434, 61, 434,
      68, 434, 436, 48, 41, 440, 48, 440, 51, 443, 9, 445, 411, 445, 418, 445, 9, 446, 385, 449,
      9, 451, 41, 450, 48, 450, 51, 450, 58, 450, 61, 450, 68, 450, 68, 453, 158, 453, 262, 453,
      408, 453, 454, 270, 454, 338, 454, 344, 158, 457, 262, 457, 408, 457, 458, 134, 458, 154, 458, 236,
      458, 370, 334, 460, 373, 460, 397, 460, 35, 462, 39, 462, 239, 462, 313, 462, 360, 462, 25, 464,
      29, 464, 35, 464, 39, 464, 464, 78, 354, 466, 387, 466, 19, 468, 39, 468, 307, 468, 328, 468,
      385, 468, 19, 470, 39, 470, 379, 472, 385, 472, 75, 474, 224, 474, 251, 474, 15, 476, 19, 476,
      171, 476, 191, 476, 208, 476, 478, 218, 478, 300, 15, 484, 19, 484, 25, 484, 29, 484, 486, 134,
      486, 236, 486, 370, 224, 489, 239, 489, 274, 489, 313, 489, 360, 489, 379, 491, 385, 491, 307, 493,
      328, 493, 35, 497, 39, 497, 39, 499, 385, 499, 379, 503, 385, 503, 61, 511, 512, 298, 512, 414,
      514, 416, 13, 517, 287, 517, 367, 517, 518, 298, 379, 521, 51, 525, 61, 525, 385, 525, 528, 134,
      528, 154, 528, 236, 528, 370, 517, 535, 517, 541, 379, 543, 501, 545, 7, 550, 51, 553, 462, 553,
      464, 553, 497, 553, 507, 553, 549, 553, 5, 554, 51, 557, 385, 557, 462, 557, 464, 557, 497, 557,
      564, 478, 385, 567, 462, 573, 497, 573, 578, 300, 580, 300, 472, 584, 51, 587, 61, 587, 143, 588,
      243, 588, 68, 591, 545, 591, 592, 6, 68, 593, 545, 595, 596, 4, 39, 598, 600, 154, 151, 603,
      39, 604, 537, 611, 379, 613, 75, 614, 171, 616, 379, 619, 15, 620, 25, 620, 51, 620, 61, 620,
      61, 623, 259, 623, 395, 623, 561, 623, 68, 625, 158, 625, 262, 625, 408, 625, 626, 420, 626, 438,
      158, 629, 262, 629, 408, 629, 630, 46, 630, 56, 630, 162, 632, 134, 632, 154, 632, 236, 632, 370,
      636, 78, 553, 636, 557, 636, 574, 640, 535, 642, 243, 648, 67, 650, 77, 650, 195, 650, 317, 650,
      533, 650, 562, 650, 650, 608, 652, 42, 48, 652, 103, 652, 201, 652, 491, 652, 495, 652, 313, 654,
      360, 654, 39, 656, 334, 659, 373, 659, 397, 659, 662, 512, 33, 665, 191, 665, 208, 665, 569, 665,
      614, 665, 670, 36, 670, 218, 15, 677, 171, 677, 570, 677, 67, 679, 77, 679, 195, 679, 317, 679,
      533, 679, 562, 679, 669, 679, 334, 681, 397, 681, 243, 683, 484, 683, 665, 685, 686, 134, 686, 154,
      686, 236, 686, 370, 476, 691, 677, 691, 694, 522, 61, 701, 468, 701, 499, 701, 700, 606, 313, 703,
      360, 703, 704, 6, 379, 707, 385, 707, 652, 707, 7, 708, 51, 711, 143, 711, 464, 711, 636, 711,
      3, 712, 51, 715, 143, 715, 149, 715, 464, 715, 636, 715, 623, 721, 722, 644, 379, 725, 517, 726,
      143, 729, 379, 731, 474, 732, 736, 630, 584, 739, 583, 740, 638, 740, 61, 742, 468, 742, 499, 742,
      334, 744, 397, 744, 249, 749, 750, 6, 68, 751, 754, 46, 753, 755, 468, 757, 499, 757, 557, 757,
      758, 2, 39, 763, 151, 765, 61, 766, 61, 769, 243, 771, 39, 773, 61, 775, 259, 775, 395, 775,
      561, 775, 721, 775, 776, 508, 776, 564, 647, 781, 782, 532, 784, 468, 39, 789, 557, 789, 158, 791,
      262, 791, 408, 791, 158, 793, 262, 793, 408, 793, 796, 66, 796, 178, 796, 264, 798, 504, 800, 134,
      800, 154, 800, 236, 800, 370, 802, 68, 804, 66, 135, 804, 237, 804, 371, 804, 804, 416, 577, 804,
      623, 804, 735, 804, 775, 804, 570, 806, 691, 806, 808, 98, 535, 808, 808, 684, 726, 808, 810, 66,
      814, 66, 689, 818, 718, 818, 820, 568, 822, 42, 57, 822, 822, 502, 531, 822, 558, 822, 822, 674,
      737, 822, 824, 42, 48, 824, 103, 824, 201, 824, 491, 824, 495, 824, 707, 824, 826, 32, 307, 828,
      328, 828, 39, 830, 832, 570, 33, 834, 191, 834, 208, 834, 836, 508, 354, 839, 387, 839, 840, 512,
      35, 843, 224, 843, 251, 843, 616, 843, 642, 845, 846, 126, 75, 849, 574, 849, 732, 849, 151, 851,
      689, 853, 718, 853, 57, 855, 531, 855, 558, 855, 737, 855, 354, 857, 387, 857, 35, 859, 224, 859,
      251, 859, 143, 861, 484, 861, 843, 863, 864, 134, 864, 154, 864, 236, 864, 370, 474, 867, 640, 867,
      849, 867, 143, 871, 483, 873, 647, 873, 851, 873, 634, 875, 667, 875, 51, 877, 462, 877, 497, 877,
      307, 879, 328, 879, 33, 881, 191, 881, 208, 881, 882, 570, 884, 4, 652, 887, 824, 887, 808, 889,
      816, 889, 5, 890, 892, 480, 808, 895, 816, 895, 61, 897, 243, 897, 816, 897, 3, 898, 61, 901,
      243, 901, 468, 901, 499, 901, 816, 901, 904, 810, 904, 814, 61, 907, 517, 908, 642, 908, 243, 911,
      476, 912, 677, 912, 804, 915, 650, 917, 679, 917, 916, 796, 916, 810, 61, 919, 249, 919, 557, 919,
      584, 919, 740, 919, 61, 920, 583, 920, 739, 920, 804, 920, 804, 921, 924, 814, 61, 927, 61, 928,
      634, 930, 667, 930, 51, 932, 462, 932, 497, 932, 354, 934, 387, 934, 35, 936, 224, 936, 251, 936,
      938, 582, 149, 941, 919, 941, 942, 4, 947, 949, 950, 2, 763, 953, 769, 953, 789, 953, 919, 953,
      143, 955, 39, 959, 161, 965, 157, 969, 195, 969, 763, 969, 769, 969, 789, 969, 957, 969, 39, 971,
      591, 971, 157, 975, 157, 979, 763, 979, 769, 979, 789, 979, 957, 979, 39, 981, 591, 981, 157, 983,
      988, 78, 135, 988, 237, 988, 371, 988, 407, 988, 988, 538, 988, 696, 988, 868, 41, 991, 48, 991,
      379, 992, 379, 995, 243, 996, 243, 999, 143, 1000, 143, 1003, 1004, 488, 1006, 658, 83, 1009, 143, 1011,
      243, 1011, 379, 1011, 41, 1012, 48, 1012, 33, 1014, 685, 1014, 385, 1017, 789, 1017, 33, 1018, 527, 1020,
      1022, 46, 143, 1024, 1026, 6, 1028, 962, 1030, 132, 9, 1033, 1032, 8, 243, 1033, 249, 1033, 379, 1033,
      385, 1033, 51, 1034, 35, 1036, 645, 1038, 957, 1043, 143, 1046, 379, 1046, 67, 1049, 283, 1049, 435, 1049,
      451, 1049, 1050, 810, 133, 1052, 1052, 810, 73, 1055, 1054, 132, 763, 1055, 769, 1055, 789, 1055, 919, 1055,
      9, 1057, 1056, 8, 9, 1058, 143, 1059, 51, 1061, 645, 1063, 1064, 154, 161, 1067, 1068, 796, 1070, 178,
      1072, 18, 1072, 716, 1074, 88, 1074, 126, 1076, 74, 1080, 16, 61, 1083, 1084, 812, 137, 1087, 553, 1089,
      557, 1089, 711, 1089, 715, 1089, 33, 1091, 685, 1091, 1090, 854, 23, 1093, 527, 1093, 1092, 852, 1094, 156,
      137, 1097, 1098, 582, 957, 1101, 143, 1103, 761, 1103, 787, 1103, 1104, 810, 83, 1107, 149, 1107, 919, 1107,
      379, 1108, 1110, 794, 379, 1113, 243, 1114, 1114, 672, 137, 1116, 1120, 36, 243, 1122, 1124, 126, 1126, 124,
      1126, 546, 1126, 660, 1128, 58, 9, 1131, 1132, 58, 31, 1134, 143, 1136, 379, 1136, 9, 1138, 493, 1140,
      1142, 796, 61, 1145, 143, 1147, 379, 1147, 9, 1149, 61, 1151, 489, 1153, 489, 1154, 897, 1154, 945, 1157,
      1158, 794, 665, 1160, 843, 1162, 1164, 8, 51, 1166, 61, 1166, 39, 1168, 39, 1170, 507, 1170, 462, 1173,
      497, 1173, 1174, 796, 31, 1176, 197, 1179, 197, 1180, 897, 1180, 27, 1182, 381, 1185, 39, 1189, 39, 1191,
      507, 1191, 945, 1193, 41, 1197, 48, 1197, 1198, 48, 1200, 48, 761, 1203, 787, 1203, 747, 1204, 1206, 8,
      379, 1208, 51, 1210, 1212, 336, 1214, 154, 659, 1217, 659, 1218, 889, 1218, 747, 1221, 9, 1223, 61, 1225,
      61, 1227, 1228, 98, 61, 1231, 39, 1232, 1234, 324, 693, 1236, 143, 1239, 157, 1239, 77, 1241, 83, 1241,
      195, 1241, 317, 1241, 453, 1241, 625, 1241, 37, 1242, 51, 1245, 121, 1245, 21, 1246, 319, 1249, 319, 1250,
      889, 1250, 693, 1253, 1254, 6, 9, 1261, 1260, 8, 11, 1262, 79, 1262, 1262, 134, 9, 1264, 161, 1267,
      9, 1268, 1270, 134, 31, 1273, 47, 1273, 73, 1273, 111, 1273, 133, 1273, 145, 1273, 169, 1273, 211, 1273,
      215, 1273, 285, 1273, 289, 1273, 565, 1273, 915, 1273, 804, 1275, 73, 1276, 169, 1276, 285, 1276, 31, 1279,
      41, 1279, 51, 1279, 61, 1279, 133, 1279, 143, 1279, 211, 1279, 61, 1280, 301, 1283, 179, 1287, 11, 1288,
      903, 1288, 89, 1291, 9, 1292, 67, 1295, 133, 1298, 9, 1301, 1302, 8, 650, 1305, 679, 1305, 1304, 796,
      1306, 814, 1308, 6, 261, 1309, 591, 1309, 665, 1310, 493, 1313, 665, 1315, 493, 1316, 89, 1318, 11, 1321,
      903, 1321, 11, 1323, 9, 1327, 61, 1328, 261, 1331, 405, 1333, 11, 1334, 83, 1339, 9, 1340, 143, 1341,
      665, 1345, 493, 1347, 39, 1349, 75, 1351, 61, 1353, 1354, 802, 1356, 56, 1356, 144, 97, 1358, 199, 1358,
      301, 1358, 367, 1358, 381, 1358, 713, 1358, 899, 1358, 1360, 16, 179, 1362, 47, 1364, 39, 1366, 75, 1368,
      67, 1370, 1372, 144, 1374, 16, 25, 1378, 245, 1382, 555, 1382, 891, 1382, 143, 1385, 497, 1385, 804, 1387,
      1388, 816, 143, 1391, 497, 1391, 379, 1392, 143, 1394, 1396, 78, 39, 1399, 650, 1401, 679, 1401, 1400, 796,
      39, 1403, 1404, 796, 233, 1407, 699, 1407, 11, 1409, 245, 1411, 555, 1411, 891, 1411, 61, 1413};
  // clang-format off
}; // namespace mockturtle

} /* namespace mockturtle */